$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $A$:Type.
\\[0ex]($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ (es{-}in{-}port(${\it es}$;$l$;${\it tg}$) $\in$ AbsInterface($A$))